Nuprl Lemma : rng_times_assoc
13,42
postcript
pdf
r
:Rng,
a
,
b
,
c
:|
r
|. (
a
* (
b
*
c
)) = ((
a
*
b
) *
c
)
|
r
|
latex
Up
rings
1
Definitions of Statement
Rng
,
r
xmn
Definitions
t
T
,
x
f
y
,
x
:
A
.
B
(
x
)
,
t
.2
,
t
.1
,
r
xmn
,
*
,
|
g
|
Lemmas
rng
wf
,
mul
mon
of
rng
wf
c
,
mon
assoc
origin
r:Rng, a, b, c:|r|. (a * (b * c)) = ((a * b) * c) 
|r| r:Rng, a, b, c:|r|. (a * (b * c)) = ((a * b) * c) |r| 
xmn Tx:A. B(x)xmn